// Module definition

module SmartCAL

// Signatures

// Entities of the Domain under exam

sig User 
{
	ownedCalendars : set Calendar ,
	sharedByOtherCalendars : set Calendar ,
	notifications : set Notification ,
	invitedEvents : set Event	
}
{
	// at least one Calendar per User
	#ownedCalendars > 0
}

sig Calendar 
{
	owner : one User ,
	allowedPeople : set User ,
	events : set Event
}
{}

sig Event 
{
	calendar : one Calendar , 
	notifications : set Notification ,
	invitedPeople : set User 
}
{}

sig Notification 
{
	event : one Event ,
	targetUser : one User
}
{}

// Facts

// No User can be invited in her own event 
fact NoAutoinvitation 
{
	no e : Event , u : User | ( u in ( e.calendar.owner & e.invitedPeople ) )  
}

// No User Calendar self-sharing
fact NoCalendarSelfSharing 
{
	no u : User | ( u in u.sharedByOtherCalendars.owner )
}

// Propert recipient for notification
fact PropertRecipientForNotification 
{
	all n : Notification | 
			( all u : User | 
						( u in n.targetUser implies 
							( u in n.event.invitedPeople  || 
							   u in n.event.calendar.owner ) ) )
}

//
fact WhatIsOwnedIsOwned_EventCalendar
{
	all e : Event , c: Calendar |
		( (e in c.events 
				implies e.calendar = c )
				and ( e.calendar =c implies e in c.events))
}

//
fact WhatIsOwnedIsOwned_UserCalendar
{
	all u : User , c: Calendar |
			( (c in u.ownedCalendars  implies c.owner = u )
			and ( c.owner = u implies c in u.ownedCalendars))
}

//
fact WhatIsOwnedIsOwned_EventNotification
{
	all n : Notification , e: Event |( (n in e.notifications  implies n.event = e )
								 and ( n.event = e implies n in e.notifications))
}

//
fact WhatIsOwnedIsOwned_Sharing
{
	all u : User , c: Calendar |( (c in u.sharedByOtherCalendars  implies u in c.allowedPeople )
								 and ( u in c.allowedPeople implies c in u.sharedByOtherCalendars))
}
// Assertions
assert ImproperRecipientForNotification
{
	no n: Notification, u: User | n.targetUser = u and ( not(u in n.event.invitedPeople) and not( u in n.event.calendar.owner))
}



check ImproperRecipientForNotification for 10
// Functions

// Returns the Calendars owned by a User
fun getOwnedCalendars [ u : User ] : set Calendar
{
	u.(ownedCalendars )
} 

// Returns the Calendars a User can access by Sharing
fun getSharedCalendars [ u : User ] : set Calendar
{
	u.sharedByOtherCalendars 
}

// Returns the Events to which a User is invited to
fun getInvitedEvents [ u : User ] : set Event
{
	u.invitedEvents 
}

// Returns the Owner of a Calendar
fun getOwner [ c : Calendar ] : lone User
{
	c.owner 
}

// Predicates

// model of the functionality that invites a User to an Event
pred addEventToUser [ u , u' : User , e : Event ] 
{
	( e not in u.invitedEvents and e.calendar.owner != u ) 
	implies ( u'.invitedEvents = u.invitedEvents + e ) 
	else ( u'.invitedEvents = u.invitedEvents )
}

run addEventToUser for 10 

// model of the behaviour of the functionality that notifies something to a User
pred addNotification [ u , u' : User , n : Notification ]
{
	n not in u.notifications implies ( u'.notifications = u.notifications + n ) 
		else ( u'.notifications = u.notifications )
}

run addNotification 

// models the adding of an event to a calendar 
pred addEventToCalendar [ c , c' : Calendar , e : Event ] 
{
	( e not in c.events ) implies ( c'.events = c.events + e ) else ( c'.events = c.events ) 
}

run addEventToCalendar for 10

pred addPersonToAnEvent [ e , e' : Event , u : User ] 
{
	( u not in e.invitedPeople ) implies ( e'.invitedPeople = e.invitedPeople + u ) 
	else ( e'.invitedPeople = e.invitedPeople )
}

// show the overall situation
pred show {}

run show for 7 
